pith. machine review for the scientific record. sign in
theorem proved term proof high

refinement

show as:
view Lean formalization →

The refinement theorem asserts that for recognizers r1 and r2 sharing configuration space C, the induced maps from the composite quotient to each component quotient are surjective. Researchers formalizing recognition composition in Recognition Science cite this when establishing that merged recognizers yield covering but finer partitions of configuration space. The proof is a one-line wrapper invoking the upstream refinement_theorem from the Composition module.

claimLet $r_1$ and $r_2$ be recognizers on a shared configuration space $C$. The natural quotient maps from the composite recognizer $r_1 ⊗ r_2$ onto the individual quotients of $r_1$ and of $r_2$ are both surjective.

background

A Recognizer pairs a configuration space C with an event space E to define observable distinctions via equivalence classes. The composite r1 ⊗ r2 merges two such recognizers on the same C, inducing a finer RecognitionQuotient. The quotientMapLeft and quotientMapRight are the canonical projections from the composite quotient to each factor quotient, constructed via Quotient.lift using the refinement relations composite_refines_left and composite_refines_right.

proof idea

The proof is a one-line wrapper that applies refinement_theorem from the Composition module, which decomposes the claim into the pair of surjectivity statements for quotientMapLeft and quotientMapRight.

why it matters in Recognition Science

This is the fundamental theorem of recognition composition, re-exported here to mirror the corresponding statement in Draft_v1.tex. It is invoked by downstream results including refinement_calibrated, refinement_discharge_inherits, and regge_sum_refinement_invariant in SimplicialLedger.CubicSimplicialEquivalence, as well as absLogVorticity in Flight.Medium. The result supports the Recognition Composition Law by guaranteeing coverage of the original quotients and feeds into simplicial refinement invariance used for Regge sums and phi-ladder calibrations.

scope and limits

formal statement (Lean)

  43theorem refinement {C E₁ E₂ : Type*} (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  44    Function.Surjective (quotientMapLeft r₁ r₂) ∧
  45    Function.Surjective (quotientMapRight r₁ r₂) :=

proof body

Term-mode proof.

  46  refinement_theorem (r₁ := r₁) (r₂ := r₂)
  47
  48end RecognitionGeometry
  49
  50/-! ## Constraint (S): Dyadic synchronization (N = 45) -/
  51
  52open Nat
  53
  54/-- The synchronization period used in `Draft_v1.tex`: `S(D) := lcm(2^D, 45)`. -/

used by (40)

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

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.