CompleteModel
plain-language theorem explainer
The CompleteModel structure extends the ledger computation model by adjoining a recognition-complete complexity pair with sub-polynomial Tc and linear Tr, a Turing specialization with vanishing recognition cost, a Clay formulation bridge, and validation data. Researchers examining ledger-induced separations between computation and recognition complexities in hypothetical P versus NP settings would reference it. The declaration is a plain structure definition with no proof obligations.
Claim. A structure extending the ledger-based computational model (state space, evolution rule, input encoding, output measurement preserving zero flux) that includes a recognition-complete complexity structure supplying sub-polynomial computation complexity $T_c$ and at least linear recognition complexity $T_r$, a Turing model specialization with zero recognition complexity, a Clay bridge that projects only onto computation complexity, and an empirical validation scaffold.
background
LedgerComputation is the base structure with states of type Type, an evolve map, encode from List Bool, and measure to Bool, enforcing closed-chain flux conservation. RecognitionComplete supplies the dual pair (Tc sub-polynomial, Tr linear). TuringModel is the special case with recognition complexity identically zero. ClayBridge maps recognition-complete data to a Turing time function while noting the projection makes P versus NP ill-posed. Validation holds measured lists confirming the predicted scalings. The module is explicitly a scaffold exploring hypothetical ledger-based complexity implications, not part of any verified certificate chain.
proof idea
Structure definition that extends LedgerComputation and packages four additional fields of the listed sibling types. No lemmas or tactics are applied; it is a direct record constructor assembling the components.
why it matters
This definition supplies the complete model object required by the downstream main_resolution theorem that asserts an unconditional P versus NP resolution through the ledger. It occupies the role of a hypothetical complete model inside the ComputationBridge scaffold module. The module documentation states the results are exploratory and must not be cited as proven mathematics or as a resolution of P versus NP. It touches the open question of whether explicit recognition costs can produce scale separation between computation and observation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.