pith. machine review for the scientific record. sign in
def definition def or abbrev high

narrative_admissible

show as:
view Lean formalization →

The narrative domain realization meets the admissibility criteria for quantified universal forcing. Researchers formalizing strict logic realizations across canonical domains cite this construction when certifying that each domain satisfies the required structural laws. The definition constructs the AdmissibleRealization instance by directly supplying its three fields via decidable cost equality, an imported associativity result, and reflexivity on the zero element.

claimLet the narrative realization have carrier the set of event states, cost function the indicator of equality (returning 0 precisely when states coincide), and composition the componentwise sum on act and beat coordinates. Then cost equality to zero is decidable for every pair of states, composition is associative, and the zero state composed with itself equals the zero state.

background

The AdmissibleRealization structure on a strict logic realization R requires three properties: cost equality to zero is decidable for any pair of carriers; the composition operation is associative; and the distinguished one element satisfies a left-identity or generator-step condition under composition. The strict narrative realization instantiates this with event states as carriers and natural-number costs, where eventCost returns 0 on equality and 1 otherwise, while eventCompose adds the act and beat components. The module elevates the five domain realizations to this typeclass so that the headline quantified universal forcing theorem applies uniformly to any admissible instance rather than to arbitrary strict realizations.

proof idea

The definition is a one-line wrapper that refines the three fields of AdmissibleRealization. The cost-decidability field is supplied by decidable equality on the eventCost function. The associativity field is taken directly from the imported eventCompose_assoc theorem for the narrative domain. The third field is discharged by reflexivity on the composition of narrativeZero with itself.

why it matters in Recognition Science

This definition supplies one of the four canonical domain witnesses collected in admissibleClassCert_holds, which in turn feeds the quantified universal forcing theorem. It verifies that the narrative realization (built on beat succession) carries the structural properties needed for the strict universal forcing equivalence to hold under the admissibility constraint. In the Recognition Science setting this step closes the gap between raw strict realizations and the admissible class over which the canonical arithmetic surfaces are forced to coincide.

scope and limits

formal statement (Lean)

  71noncomputable def narrative_admissible : AdmissibleRealization Narrative.strictNarrativeRealization := by

proof body

Definition body.

  72  refine ⟨?_, ?_, Or.inl ?_⟩
  73  · intro a b; exact decEq (Narrative.eventCost a b) 0
  74  · exact RichDomainCosts.NarrativeRich.eventCompose_assoc
  75  · show Narrative.eventCompose Narrative.narrativeZero Narrative.narrativeZero
  76        = Narrative.narrativeZero
  77    rfl
  78

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.