Proof-Backed Showcase

Claim boundary advertised theorem ids are proved examples are support no open-problem progress claim

This page is the public-facing capability map for Circle Calculus. It is allowed to be inviting, but it is not allowed to float free of the proof corpus.

Every advertised item below is backed by manifests/capability_showcase.yaml. The validator scripts/check_capability_showcase.py requires each item to cite known papers, proved theorem ids, dictionary ids, source files, and pytest-discovered executable examples. The generated-data checker then recomputes the portfolio summary from those capability rows: every advertised theorem id must be carried by a cited paper, every advertised source ref must be backed by a cited paper Source Trail or cited Lean sidecar import closure, and every Living Book ref must carry the advertised page/widget evidence. If any theorem is unproved, unknown, not carried by the cited papers, not traceable to cited source evidence, or absent from its Living Book presentation, the checks fail.

This page advertises expressiveness and proof-linked interfaces. It does not upgrade executable examples, benchmark fixtures, imported theorem bridges, or roadmap ideas into new mathematical proofs.

Why This Page Exists

Circle Calculus should be judged by whether it can express serious structures in a way that is readable, executable, and formally auditable. The strongest current answer is not one slogan. It is a portfolio of checked handles:

  • famous additive-combinatorics theorems stated in circle vocabulary,
  • extremal and Ramsey theorem bridges with small finite examples,
  • detailed modular period/fiber arithmetic,
  • bounded quaternion and Hopf phase facts,
  • finite gauge-path and holonomy interfaces,
  • proof-carrying generated structures,
  • cyclic AI schedule/index facts, and
  • cyclic compute layout facts.

The generated matrix starts with four proof-backed reader routes: hard mathematics bridges, the cyclic proof spine, phase/finite-physics interfaces, and proof-carrying generated/AI structures. A route is ready only when every listed capability is known, fully claim-contracted, backed for its declared role, connected by an ordered proof trail, packaged as a skeptical-reader review packet, tied to a generated standard-parity/Circle-native-value comparison, bundled into a route-level reviewer dossier, summarized by a generated impact summary, and backed by the same theorem/source/Living Book evidence used below.

Hard Mathematics Bridges

Zero-Sum And Sumset Theorems

Circle Calculus states EGZ and Cauchy-Davenport directly over C_n and C_p.

Paper: Zero-Sum Circles

  • Portfolio roles: standard_math_parity; circle_native_value.
  • Standard anchor: Classical zero-sum and additive-combinatorics theorems over cyclic groups, especially EGZ and Cauchy-Davenport.
  • Circle expression: Finite circle types C_n and C_p present the cyclic groups directly, with theorem ids for zero-sum subsequences and prime-circle sumset growth.
  • Circle-native value: The Circle framing makes zero-sum witnesses, sharpness families, and sumsets inspectable as finite address-space examples linked to Lean and Python sidecars.
  • Advertised claim: Circle Calculus can state established zero-sum and prime-circle sumset theorems directly in the native C_n vocabulary.
  • Executable evidence: sidecars/PAPER_ERDOS_01_ZERO_SUM_CIRCLES/python/test_zero_sum_circle_examples.py.
  • Vocabulary evidence: CC-0001; CC-0201.
  • Living Book evidence: site/chapters/applications/erdos_bridges.qmd.
  • Scope: Lean-proved Circle wrappers around mathlib’s EGZ and Cauchy-Davenport theorems.
  • Proof provenance: Proof provenance is a Circle wrapper over mathlib-formalized EGZ and Cauchy-Davenport, with Circle-specific examples and vocabulary layered on top.
  • Boundary: No new proof of EGZ, no new proof of Cauchy-Davenport, and no progress claim on an open Erdos problem.

Katona And Erdos-Ko-Rado

The Katona lane makes cyclic-order double counting and intersecting-family bounds visible while keeping the theorem source formal.

Paper: Katona and Erdos-Ko-Rado

  • Portfolio roles: standard_math_parity; circle_native_value.
  • Standard anchor: The Katona circle method and the Erdos-Ko-Rado theorem for intersecting uniform set families.
  • Circle expression: Numberings, prefix-density counts, and intersecting families are exposed as theorem-backed finite-circle-method artifacts.
  • Circle-native value: The project can show the circle-method proof atom as an executable finite count, then connect it to a formal EKR theorem card.
  • Advertised claim: Circle Calculus can expose a classical circle-method counting atom and the Erdos-Ko-Rado bound as proof-linked artifacts.
  • Executable evidence: sidecars/PAPER_ERDOS_02_KATONA_EKR_CIRCLE_METHOD/python/test_katona_ekr_examples.py.
  • Vocabulary evidence: CC-0001; CC-0201.
  • Living Book evidence: site/chapters/applications/erdos_bridges.qmd.
  • Scope: Lean-proved wrappers around mathlib’s Katona prefix-density and Erdos-Ko-Rado declarations.
  • Proof provenance: Proof provenance is a Circle wrapper over mathlib-formalized Katona and Erdos-Ko-Rado declarations, plus finite Circle-method examples.
  • Boundary: No new EKR proof and no classification of all extremal families.

Roth And Three-Term Progressions

The Roth lane gives Circle Calculus a serious density-additive-combinatorics target with finite witness searches as examples.

Paper: Roth and Three-Term Progressions

  • Portfolio roles: standard_math_parity; circle_native_value.
  • Standard anchor: Roth’s theorem and the asymptotic sublinearity of maximal three-term-AP-free subsets of natural intervals.
  • Circle expression: Dense finite interval examples and AP witness searches are connected to formal Roth theorem handles.
  • Circle-native value: Circle Math supplies a bridge toward cyclic AP models while keeping finite witness search, density claims, and Lean theorem status separated.
  • Advertised claim: Circle Calculus can connect finite witness searches to formal Roth-theorem handles.
  • Executable evidence: sidecars/PAPER_ERDOS_03_ROTH_THREE_AP_CIRCLES/python/test_roth_three_ap_examples.py.
  • Vocabulary evidence: CC-0001; CC-0201.
  • Living Book evidence: site/chapters/applications/erdos_bridges.qmd.
  • Scope: Lean-proved wrappers around mathlib’s Roth theorem and Roth-number sublinearity statement.
  • Proof provenance: Proof provenance is a Circle wrapper over mathlib-formalized Roth handles, with project finite-witness examples kept separate from the proof.
  • Boundary: No new Roth proof, no improved bounds, and no cyclic-to-natural transfer theorem yet.

Ramsey Lines And Hales-Jewett

The Ramsey lane shows unavoidable structure through formal Hales-Jewett and homothetic-copy handles.

Paper: Hales-Jewett and Ramsey Lines

  • Portfolio roles: standard_math_parity; circle_native_value.
  • Standard anchor: Hales-Jewett and Van der Waerden style unavoidable monochromatic-line or homothetic-copy theorems.
  • Circle expression: Finite coloring examples and combinatorial-line widgets can be attached to Lean theorem ids for the general Ramsey statements.
  • Circle-native value: The Circle presentation can turn unavoidable structure into inspectable finite search artifacts without confusing examples for proofs.
  • Advertised claim: Circle Calculus can present Ramsey-style unavoidable structure with theorem ids and executable finite searches.
  • Executable evidence: sidecars/PAPER_ERDOS_04_HALES_JEWETT_RAMSEY_CIRCLES/python/test_ramsey_hj_examples.py.
  • Vocabulary evidence: CC-0001; CC-0201.
  • Living Book evidence: site/chapters/applications/erdos_bridges.qmd.
  • Scope: Lean-proved wrappers around mathlib’s Hales-Jewett and homothetic-copy theorems.
  • Proof provenance: Proof provenance is a Circle wrapper over mathlib-formalized Ramsey/Hales-Jewett style theorems, with finite searches used only as examples.
  • Boundary: Finite Python searches are examples only; they are not the Hales-Jewett proof.

Circulant Graph Geometry

The graph lane starts conservatively with cycle graphs, circulant graphs, connectedness, and unit-distance vocabulary.

Paper: Unit-Distance Circulant Graphs

  • Portfolio roles: standard_math_parity; circle_native_value.
  • Standard anchor: Standard cycle graphs, circulant graphs, graph connectedness, and unit-distance embedding vocabulary.
  • Circle expression: The one-step finite circle graph is presented as a circulant graph, with connectedness and a minimal unit-distance embedding constructor.
  • Circle-native value: The graph lab makes cyclic graph structure explicit before moving to harder Euclidean incidence questions.
  • Advertised claim: Circle Calculus can use cyclic graph models as a proof-backed bridge toward graph-geometry language.
  • Executable evidence: sidecars/PAPER_ERDOS_05_UNIT_DISTANCE_CIRCULANT_GRAPHS/python/test_circulant_graph_examples.py.
  • Vocabulary evidence: CC-0001; CC-0201.
  • Living Book evidence: site/chapters/applications/erdos_bridges.qmd.
  • Scope: Lean-proved cycle/circulant and connectedness bridges plus a unit-distance embedding constructor for empty graphs.
  • Proof provenance: Proof provenance is project-native Lean code for cyclic graph structures and a minimal unit-distance embedding constructor, aligned with standard graph vocabulary.
  • Boundary: No progress on hard unit-distance or distinct-distance problems.

Circle-Native Strengths

Periods, Fibers, Kernels, And Normal Forms

The S1 spine is the internal proof engine: period, gcd orbit count, scaling images, fibers, kernel representatives, and full-coil conditions.

Paper: Finite Circles

Paper: Factors, Scaling, Prime Coils

  • Portfolio roles: standard_math_parity; circle_native_value.
  • Standard anchor: Standard modular arithmetic, cyclic group orbits, gcd periods, kernels, images, and fibers of multiplication maps.
  • Circle expression: The S1 theorem spine expresses these facts as finite-circle period, orbit, scaling, image, kernel, and fiber theorems.
  • Circle-native value: Circle Math organizes modular facts around movement, closure, fibers, and representatives, making them easier to browse and test.
  • Advertised claim: Circle Calculus can express detailed modular-arithmetic structure as period, orbit, kernel, and fiber theorems.
  • Executable evidence: sidecars/PAPER_S1_04_FACTORS_SCALING_PRIME_COILS/python/test_paper_s1_04_examples.py.
  • Vocabulary evidence: S1-0001; CC-0105; CC-0205; CC-0207; COMMON-0041.
  • Living Book evidence: site/chapters/S1/03_coils_orbits_closure.qmd; site/chapters/S1/04_period_gcd_prime_full_coils.qmd; widgets coil_orbit_explorer, period_gcd_visualizer, prime_full_coil_explorer.
  • Scope: Lean-proved S1 scaling and orbit spine, including full-coil iff coprime and image-times-fiber factorizations.
  • Proof provenance: Proof provenance is project-native Lean code in the S1 finite-circle spine, backed by paper and Python sidecar examples.
  • Boundary: No claim that this replaces standard modular arithmetic; it is a proof-carrying cyclic presentation.

Quaternion And Hopf Phase Coordinates

The S3 lane gives bounded phase-coordinate, quaternion, pure-vector, and spin-sign facts that are useful for rotation, hidden phase, and sign-ambiguity explanations.

Paper: Quaternion Coils

Paper: Hopf Coils

Paper: Spin Double Cover Roadmap

  • Portfolio roles: standard_math_parity; circle_native_value.
  • Standard anchor: Quaternion unit algebra, Hopf-style phase coordinates, conjugation, and hidden phase symmetries.
  • Circle expression: Quaternion, spin-sign, pure-vector, real Hopf-coordinate, and common-phase invariance facts are exposed through theorem spines with explicit topology warnings.
  • Circle-native value: The Circle framing separates visible base coordinates from hidden phase in a way that is useful for teaching, widgets, and proof audits.
  • Advertised claim: Circle Calculus can express quaternion, spin-sign, pure-vector, real Hopf-coordinate, and common-phase invariance facts with explicit warnings about topology boundaries.
  • Executable evidence: sidecars/PAPER_S3_02_QUATERNION_COILS/python/test_quaternion_coil_examples.py; sidecars/PAPER_S3_03_HOPF_COILS/python/test_paper_s3_03_examples.py; sidecars/PAPER_S3_04_SPIN_DOUBLE_COVER_ROADMAP/python/test_spin_conjugation_examples.py.
  • Vocabulary evidence: S3Q-0001; S3H-0001; S3H-0002; S3S-0001; S3S-0002; S3S-0003.
  • Living Book evidence: site/chapters/S3/hopf_coils.qmd; site/chapters/applications/physics.qmd; widgets hopf_hidden_phase, spin_sign_ambiguity.
  • Scope: Lean-proved quaternion unit laws, pure-vector conjugation boundary, sign-cancellation facts, exact real-unit kernel facts for conjugation, real Hopf landing, and common-phase invariance facts.
  • Proof provenance: Proof provenance is project-native Lean code for quaternion, spin-sign, pure-vector, real Hopf-coordinate, and common-phase invariance facts, with topology limits stated explicitly.
  • Boundary: No full smooth Hopf fibration formalization and no complete SO(3) robotics formalization.

Application Interfaces

Finite Gauge Paths

The physics lane builds proof-carrying finite gauge paths with checked path composition and holonomy interfaces.

Paper: Proof-Carrying Lattice Gauge

  • Portfolio roles: standard_math_parity; circle_native_value; application_guardrail.
  • Standard anchor: Discrete gauge-link paths, holonomy products, Wilson-loop style invariants, and checked path concatenation.
  • Circle expression: Finite gauge links and paths are represented with Lean-checked source-target and holonomy laws.
  • Circle-native value: Circle Math contributes proof-carrying finite records that can guard simulations and widgets against invalid path composition.
  • Advertised claim: Circle Calculus can build a finite proof-carrying gauge-path model with endpoint and holonomy laws.
  • Executable evidence: sidecars/PAPER_PHYS_01_PROOF_CARRYING_LATTICE_GAUGE/python/test_lattice_gauge_examples.py.
  • Vocabulary evidence: COMMON-0060; COMMON-0061; COMMON-0062; COMMON-0063.
  • Living Book evidence: site/chapters/applications/physics.qmd; widgets finite_path_algebra, finite_gauge_loop_holonomy, wilson_loop_certificate.
  • Scope: Lean-proved finite link-path, checked-path, path-plus-reverse zero-holonomy, gauge-transform, Wilson-loop, plaquette, closed-loop record, gauge-shifted closed-loop, closed-loop gauge-sample independence, two-path cycle gauge-invariance, two-path basepoint-swap facts, and complete cyclic three-path cycle basepoint-rotation packages.
  • Proof provenance: Proof provenance is project-native Lean code for finite gauge-link/path records and holonomy laws, with Python fixtures serving as executable references.
  • Boundary: No continuum gauge theory, no physics discovery, and no lattice-QCD correctness claim.

Generative Provenance

The generative lane pairs seed-rule construction with exact-regeneration checks and negative-case gates.

Paper: Seed-Rule Provenance

Paper: Proof-Carrying Glyphs

  • Portfolio roles: circle_native_value; application_guardrail.
  • Standard anchor: Formal provenance, exact regeneration checks, orbit decompositions, and proof-carrying artifact records.
  • Circle expression: Seed rules, generator comparisons, proof glyphs, and exactness gates are expressed as finite Circle records and Lean facts.
  • Circle-native value: This is a Circle-native value proposition: generated artifacts can carry exact source trails and negative-case checks instead of loose visual claims.
  • Advertised claim: Circle Calculus can pair generated structures with checked provenance and exact-comparison gates.
  • Executable evidence: sidecars/PAPER_GEN_01_SEED_RULE_PROVENANCE/python/test_seed_rule_provenance_examples.py; sidecars/PAPER_P2_05_PROOF_CARRYING_GLYPHS/python/test_proof_glyph_examples.py.
  • Vocabulary evidence: COMMON-0033; COMMON-0064; COMMON-0065; COMMON-0066.
  • Living Book evidence: site/chapters/applications/generative.qmd; widgets seed_rule_diagram_generator, orbit_family_generator, proof_glyph_certificate, generator_comparison_search.
  • Scope: Lean-proved seed-rule, finite-circle node membership/no-duplicate/nonempty, orbit-decomposition, proof-glyph, generated-list length, exact-regeneration, negative-case, empty declared-search boundary, singleton exact-search, best-candidate soundness, exact-candidate absence/count gates, exact-candidate list soundness, singleton membership gates, finite-search count guardrails, and finite storage-accounting checks for the public C_128 fixture.
  • Proof provenance: Proof provenance is project-native Lean code for seed-rule provenance, proof glyphs, exact-regeneration gates, and negative-case search boundaries.
  • Boundary: No universal compression claim and no guarantee that generated artifacts are mathematically interesting.

AI Schedules And Index Safety

The AI lane proves finite schedule/index facts that can support experiments without pretending proofs imply model quality.

Paper: Coil Attention And Memory

Paper: CoilRA And MultiCoil RoPE

  • Portfolio roles: standard_math_parity; circle_native_value; application_guardrail.
  • Standard anchor: Finite cyclic buffers, schedule normalization, recurrence budgets, sparse strided attention, RoPE relative phase, MultiCoil phase-pair closure, residue/winding position bookkeeping, circular convolution, and modular adapter indexing.
  • Circle expression: AI-facing memory slots, loop budgets, exit certificates, looped recurrent states, middle-block routes, combined route/budget schedules, strided, hybrid, and stride-family sparse-attention reachability, RoPE relative phase, MultiCoil phase-pair product-cycle closure, residue-plus-winding position records, circulant mixer laws, block-cyclic mixer cells, and adapter blocks are encoded as finite cyclic address/schedule theorems.
  • Circle-native value: Circle Math can make experimental cyclic AI components auditable before any model-quality or speed claim is made.
  • Advertised claim: Circle Calculus can prove finite indexing, schedule-safety, single-stride/hybrid/stride-family sparse-coverage, relative-phase, MultiCoil product-cycle closure, residue/winding reconstruction, circulant-mixer structure, and block-cyclic shared-cell facts that AI experiments can reuse.
  • Executable evidence: sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/test_memory_slot_examples.py; sidecars/PAPER_AI_03_COILRA_AND_MULTICOIL_ROPE/python/test_adapter_block_examples.py.
  • Vocabulary evidence: COMMON-0028; COMMON-0029; COMMON-0030; COMMON-0031; COMMON-0047; COMMON-0052; COMMON-0067; COMMON-0068; COMMON-0071; COMMON-0072; COMMON-0073; COMMON-0074; COMMON-0075; COMMON-0079; COMMON-0081.
  • Living Book evidence: site/chapters/applications/ai.qmd; site/chapters/applications/looped_recurrence_contracts.qmd; widgets cyclic_memory_slots, loop_recurrence_budget, loop_exit_certificate, token_level_recurrence, training_free_loop_wrapper, learned_token_recurrence, learned_middle_block_recurrence, learned_multi_resolution_recurrence, learned_recurrence_schedule, stride_family_attention, adapter_parameter_budget, circulant_mixer_validation, block_cyclic_mixer_validation, multicoil_phase_explorer, winding_aware_position.
  • Scope: Lean-proved finite memory-slot, loop-budget, active-token-step, looped recurrent-state, positive raw-budget closure, middle-block route, combined route/budget one-cycle and multi-cycle common-cycle closure, sample-zero route/budget initialization, recurrence-budget positivity, unavailable-budget clamp, loop-exit, score-trace first-active iff, budgeted first-active existence iff, certificate-availability, certificate-budget-selection, certificate multi-pass invariance, generated-live-window KV request contracts, strided-attention coverage, local/coil/hybrid sparse-attention reachability, finite stride-family sparse-attention reachability, stride-family gap and complete-coverage certificates, raw/context-clipped candidate-budget bounds, theorem-side lag-candidate membership semantics, query-indexed candidate-list/count semantics, lag-side and query-side unique-count shortfall iff gap endpoints, period-threshold lag/query shortfall iff endpoints, zero-residue period-violation witness iff, no-zero failure iff endpoints, first-alias period witness facts, zero-residue alias-count and total-count formulas, public 4096 no-wrap and 8192 coprime planner covered/uncovered and query-side exact-count facts, lag/query dedup-loss zero/positive iff no-collision/collision endpoints, lag/query unique-plus-loss-equals-raw accounting endpoints, lag/query collision-pair count fixture facts, zero/positive iff endpoints, and pair-count-bounds-dedup-loss severity inequalities, no-collision candidate-count equality, structural, singleton no-wrap numeric, singleton/family no-zero period-threshold, compositional multi-stride, numeric head/tail separation, ordered separated-family residue, separated-family local/lag no-collision, separated-family query/raw-budget no-collision sufficient conditions, and numeric predecessor-injectivity sufficient conditions, RoPE relative-phase invariance, two-period MultiCoil phase-pair bounds/product-cycle closure, residue/winding position reconstruction, circulant shift-equivariance/commutativity/additivity, shift-action, block-cyclic row/column residue-cell closure, and adapter-block normalization facts.
  • Proof provenance: Proof provenance is project-native Lean code for finite cyclic memory, loop-budget, looped recurrent-state, positive raw-budget closure, active-step, score-trace first-active semantics, middle-block route, combined route/budget common-cycle and sample-zero initialization, certificate, strided, hybrid, and stride-family sparse-attention reachability/gap/budget/candidate-list/period-witness, collision-pair boundary/severity, and per-stride/family-total alias-count semantics, RoPE relative phase, MultiCoil product-cycle closure, residue/winding position reconstruction, circulant mixer laws, block-cyclic shared-cell laws, and adapter-index safety facts; benchmarks remain separate.
  • Boundary: No model-quality, speed, context-length, or reasoning improvement claim without benchmark evidence.

Circular Compute Layouts

The compute lane proves address-safety and schedule-normalization facts before any backend performance claim is allowed.

Paper: Circular Computation

Paper: Coil Layout Stencil NTT

Paper: Coil Systems Applications

  • Portfolio roles: standard_math_parity; circle_native_value; application_guardrail.
  • Standard anchor: Circular buffers, periodic stencils, stride-address formulas, and round-robin scheduling laws.
  • Circle expression: Compute layouts are expressed as finite address normalization, stride-address, and schedule-preservation theorems.
  • Circle-native value: The Circle form can certify when cyclic structure is real enough to justify backend experiments, while requiring benchmarks for performance claims.
  • Advertised claim: Circle Calculus can prove finite address-safety and schedule-normalization facts for cyclic computation.
  • Executable evidence: sidecars/PAPER_COMP_01_PROOF_CARRYING_CIRCULAR_COMPUTATION/python/test_cyclic_address_examples.py; sidecars/PAPER_COMP_03_COIL_LAYOUT_STENCIL_NTT/python/test_stride_address_examples.py; sidecars/PAPER_COMP_04_COIL_SYSTEMS_APPLICATIONS/python/test_round_robin_slot_examples.py.
  • Vocabulary evidence: COMMON-0018; COMMON-0022; COMMON-0040; COMMON-0045.
  • Living Book evidence: site/chapters/applications/compute.qmd.
  • Scope: Lean-proved cyclic-address, stride-address, and round-robin schedule laws with Python layout fixtures.
  • Proof provenance: Proof provenance is project-native Lean code for cyclic-address, stride-layout, and round-robin schedule laws, with performance claims left to explicit benchmarks.
  • Boundary: No performance claim without direct dense, FFT/NTT, and backend baselines.

Verification Contract

The showcase source is:

manifests/capability_showcase.yaml

The validator is:

python scripts/check_capability_showcase.py

That check is part of make sourcecheck, so the advertised surface is kept under the same proof-status discipline as the rest of the project.