Sectors
11
E · M · S · F · W · T · I · R · H · P · A
Finite atlas · Lean formalization
Explore the 165
three-sector charts.
A searchable expansion of the eleven-sector triplet atlas, paired with a small interactive calculator for the scalar coupling model formalized in Lean.
Model boundaryThis dashboard expands the combinatorial atlas and evaluates one scalar residual formula. The full physical equation source and the definitions needed for an Einstein or matter field solver are not included in this repository.
Triplets
165
all unordered 3-sector subsets
Grammar slots
585
expected statements across triplets
Proved properties
7
FS-T01 through FS-T07 in Verified.lean
Six structural profiles
Profile counts correspond to the finite partition in
Verified.lean.Triplet atlas
Select any chart to inspect its sector kinds and expected statement inventory.
Scalar residual calculator
Enter values for the generic coefficients and fields below. This evaluates the algebraic expression from Coupling.lean; it does not infer coefficients from the atlas or solve a differential equation.
Algebra demonstrator · not a physical solver
R = base + λᵢⱼ φⱼ + λᵢₖ φₖ + λᵢⱼₖ φⱼ φₖ
Residual9
Full expression R17
φₖ = 0 · third-field slice7
Remove λᵢⱼₖ term · ablation3
What the proofs establish
The Lean theorems establish finite-set counts, incidence, profile partition, ablation cardinality, overlap counts, and a narrow shared-bilinear-term reciprocity lemma. The 585 total is a theorem about the defined statement grammar; source-file auditing is a separate task.
What remains to validate
The repository's repair schedule records package-layout and import issues that currently prevent a clean fresh-clone build. Physical interpretation also needs complete typed equations, assumptions, units, predictions, and reproducible empirical tests.