Generative Structures
This lesson treats an object as something that can be regenerated from a seed, rules, a schedule, and a closure condition.
The ordinary baseline is value-only storage:
list every node
list every orbit element
list every diagram field
list every physics-loop edge
The Circle Calculus version records the construction:
seed + rule set + schedule + closure condition
-> generated object
-> theorem ids
-> dictionary ids
-> regeneration check
A generator record is not automatically smaller, optimal, or more meaningful. Its Python fixtures are executable references, not proof artifacts. It is useful only when exact regeneration, reader clarity, or proof linkage improves.
Showcase evidence: SHOW-009 proof-carrying generative provenance.
What You Should Learn
By the end of the page, you should be able to explain why C_128 can be clearer as a seed-rule record while C_1 can be clearer as an explicit object.
Ordinary Baseline
Explicit storage is straightforward. For a finite circle, store all nodes. For a coil, store the entire orbit. For a proof glyph, store the final displayed metadata. That baseline is important because the generator has to beat or explain something real.
Circle Calculus Framing
Coils already have a generative shape:
start node
-> stride rule
-> repeated rotation
-> closure
Seed-rule provenance makes the construction explicit. The generated object still exists, but it is paired with the record that rebuilt it and the theorem/dictionary ids that explain what the record means.
Executable Fixture
The Python reference model under circle_math/generative.py provides:
SeedRuleProvenance
finite_circle_generator
finite_circle_diagram_generator
physics_loop_diagram_generator
coil_orbit_generator
orbit_decomposition_generator
proof_glyph_generator
regenerate
compare_generator_to_explicit
bounded_generator_search
The sidecar tests regenerate finite circle nodes, a finite-circle diagram with successor edges, a finite physics-loop diagram with normalized plaquette phases and holonomy, a stride orbit, the full stride-orbit decomposition, and proof-glyph metadata. The comparison fixture checks exact regeneration before comparing description length. The bounded search fixture ranks only an explicitly supplied finite candidate list; it does not claim global minimality. The current Lean spine proves both the empty-search boundary and the soundness boundary for any returned best exact candidate. The widget below reads site/data/generated/generator_index.json, which is exported from the Python seed-rule fixtures, and exposes finite-circle, finite physics-loop, coil-orbit, orbit-family, and proof-glyph records as generated explanation with theorem-status badges pulled from the manifest.
The orbit-family widget narrows that broad generator view to one important case: generate each stride orbit, restart at the smallest unvisited node, and stop only when the family covers the finite circle exactly once.
The proof-glyph certificate widget focuses on the theorem-navigation part of the same generator contract. It reads a generated glyph record, checks that the theorem id resolves in the manifest, and checks that the generated Lean declaration name matches the manifest entry. This is proof navigation, not the proof itself.
The next widget focuses on the compression reframing directly. It compares explicit object storage with a seed-plus-rule record, includes a broken non-exact candidate, and reports bounded-search scope. It is a finite fixture, not an optimal-compression theorem.
The public Circle AI contract pack exports the same bounded-search boundary as machine-readable evidence. A downstream project can read:
bounded_search_candidate_count = 3
bounded_search_exact_candidate_count = 2
bounded_search_has_best_exact = true
bounded_search_has_best_shorter = true
bounded_search_candidate_ids_by_generator_length =
finite_circle_unit_fixture,
finite_circle_broken_fixture,
finite_circle_public_fixture
bounded_search_best_exact_candidate_id = finite_circle_unit_fixture
bounded_search_best_shorter_candidate_id = finite_circle_public_fixture
The theorem-backed part is the finite accounting: exact candidates cannot outnumber declared candidates (GEN-T0044), a positive exact count is equivalent to the existence of a best exact candidate (GEN-T0037), and any returned best exact candidate implies a nonempty declared search space (GEN-T0045). This still says nothing about global minimality.
The generic AI contract pack exposes this as two copy-safe recommendation records. SEED-RULE-USE-EXACT-REGENERATION-RECIPE names the public finite-circle seed/rule recipe, and SEED-RULE-SELECT-BOUNDED-SHORTER-CANDIDATE names the shorter exact candidate inside the declared finite search. A downstream project can read them with python scripts/circle_ai_contract_ready.py --kind seed_rule_exact_regeneration --digest --field storage_saving --include-recommendations. The candidate ids matter because several declared records share artifact_id=finite_circle: the unit fixture is the smallest exact generator by description length, while the public C_128 fixture is the exact generator that actually saves storage under the declared metric. These are fixture-level generator/provenance records, not global minimality, Kolmogorov-complexity, compression, semantic-equivalence, or model-quality claims.
Run the public certifier directly:
python scripts/seed_rule_certify.py
python scripts/seed_rule_certify.py --n 8
python scripts/seed_rule_certify.py --format jsonWhy should exact regeneration be checked before reporting that a generator is shorter than an explicit object?
Positive And Negative Cases
For a large finite circle, storing the seed n plus the rule “generate nodes 0 through n-1” is shorter than listing every node. For a one-node circle, the provenance metadata is longer than the object itself.
Both results are useful. The positive case shows constructive compression. The negative case prevents overclaiming.
Proof Boundary
Read these in two honest tiers. The substantive facts are the orbit and regeneration theory: GEN-T0003 and GEN-T0006–GEN-T0013 (orbit count, period, coverage, formal orbit-class agreement, canonical-representative coverage and disjointness — the same non-trivial gcd/orbit spine as S1) and GEN-T0014–GEN-T0019 (exact regeneration as a reflexive/symmetric/transitive relation). The remaining GEN-T0020–GEN-T0050 are elementary bookkeeping — generated-list lengths and finite-search bounds (empty search returns nothing, a returned candidate lies in the declared list, counts are bounded) plus finite storage accounting for one declared C_128 fixture. Those are honest and keep the search and contract code sound, but they are the trivial finite-closure family, not evidence of global minimality or a universal compression win. And the fixtures are exploratory: a generator record is not automatically a compression win.
The theorem cards below are representative audit handles. GEN-T0003 proves exact regeneration of the representative-indexed orbit-schedule list. GEN-T0013 closes the canonical orbit-family disjointness fact. GEN-T0019 makes field equality sufficient for exact regeneration. GEN-T0025 proves that a returned best exact candidate belongs to the declared exact list. GEN-T0040 and GEN-T0045 are finite generation and bounded-search guardrails. GEN-T0046 and GEN-T0050 expose the public storage-accounting contract boundary. The full theorem-card trail lives in the Generative Structures Proof Audit.
Dictionary Trail
Source Trail
Generative paper: Seed-Rule Provenance
S1 source paper: Factors, Scaling, And Prime Coils
Glyph paper: Proof-Carrying Glyphs
Physics source paper: Proof-Carrying Finite Lattice Gauge Links
The Python fixture is an executable reference. The formal path is to encode exact finite regeneration facts in Lean and keep description-length comparisons separate from optimal-compression claims.