DeltaFactorizationCharacterTheoryCertificate
plain-language theorem explainer
A Prop-valued ledger packaging every certificate on the factorization character-theory lane: chart transitions, residue orbits, unit groups, period spectrum and existence, finite multiplicative characters, goal closure, coordinate uniqueness, period factors, even-period gaps, and substrate dichotomy. Anyone citing the master factorization certificate uses this bundle as the typed checklist. As a structure definition there is no proof; the companion theorem fills each field by named sub-certificates.
Claim. The factorization character-theory ledger is the conjunction of: chart-transition obstruction, residue-orbit, unit-group, period-spectrum, finite multiplicative character, recognition lower bound, physical period readout interface, prime-coordinate transform interface, D4 goal closure (native noncomputable $\delta$-choice), coordinate uniqueness, period factor, period existence, even-period-gap reduction, and substrate dichotomy.
background
In the Primitive Recognition Calculus factorization lane, each layer is sealed by a small Prop structure called a certificate. Certificates record proved identities and interfaces without smuggling unfinished goals. The chart-transition certificate asserts that factor-pair products display ordinary natural multiplication and equal products share magnitude. The period-existence certificate asserts that the Euler period returns the unit residue and that a period exists for unit residues. The even-period-gap certificate records a conditional reduction from an even-period witness to a nontrivial factorization, explicitly not supplying existence.
Goal closure (D4) states that the residual prime-coordinate readout is closed by a native noncomputable $\delta$-choice transform, with classical transport kept on a separate proved path. Coordinate uniqueness ties prime orbits on distinction naturals to ordinary primality. Finite multiplicative characters supply the principal character and its multiplicativity on unit residues.
This module sits at the top of that stack: it does not prove new arithmetic; it names the full conjunction the character-theory lane claims to have closed.
proof idea
No proof body: the declaration is a structure of type Prop whose fields are the named sub-certificates. Inhabitation is deferred to the companion theorem that assigns each field by the corresponding proved certificate (chart transition, residue orbit, unit group, period spectrum, and so on). Treat the structure as a typed checklist, not an argument.
why it matters
This ledger is the typed master interface for the factorization character-theory lane. The sole direct consumer is the theorem that builds a concrete instance by wiring every sub-certificate into the fields. Downstream work that needs the whole character-theory package cites that instance rather than re-listing fourteen separate certificates.
In Recognition Science terms the lane supports the discrete arithmetic substrate behind recognition periods and prime-coordinate readouts: period spectrum and existence, even-period gaps, and substrate dichotomy sit under the broader forcing story that isolates discrete octave structure (eight-tick / $2^3$ themes) and unique coordinates. Goal closure records that factor recovery is sealed by native $\delta$-choice, keeping classical transport separate. The structure itself closes no open arithmetic question; it only freezes the checklist so the master certificate can be stated in one line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.