Canonical Admissible Fiber Decomposition

Abstract

A readout canonically decomposes all states and admissible states into dependent fibers.

Definition 1.1 (Admissible concept fiber).

$$\forall X,B:\mathrm{Type},q:X\to B,Adm:X\to \mathrm{Prop},b:B,\mathrm{AdmissibleConceptFiber}\left(q,Adm,b\right)=\sum _{x:X}Adm(x)\wedge q(x)=b.$$

Formalization. D5/S3/ConceptDynamics/Fibers/CanonicalAdmissibleFiberDecomposition.AdmissibleConceptFiber (✓ std3).

Source. Repository-derived.

Commentary.

The admissible fiber over b contains a state x, evidence that x is admissible, and an equality q(x) = b.

Theorem 1.2 (Ordinary and admissible states decompose into canonical fibers).

$$\begin{array}{c}\forall X,B:\mathrm{Type},\\ q:X\to B,Adm:X\to \mathrm{Prop},\\ \exists !e:X\equiv \sum _{b:B}\mathrm{ConceptFiber}\left(q,b\right),\forall x:X,e(x)=⟨q(x),⟨x,refl⟩⟩\wedge \forall b:B,x:X,p:q(x)=b,e^{-1}(⟨b,⟨x,p⟩⟩)=x\wedge \\ \exists !e_{Adm}:\sum _{x:X}Adm(x)\equiv \sum _{b:B}\mathrm{AdmissibleConceptFiber}\left(q,Adm,b\right),\forall x:X,h:Adm(x),e_{Adm}(⟨x,h⟩)=⟨q(x),⟨x,h,refl⟩⟩\wedge \forall b:B,x:X,h:Adm(x),p:q(x)=b,e_{Adm}^{-1}(⟨b,⟨x,h,p⟩⟩)=⟨x,h⟩.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/CanonicalAdmissibleFiberDecomposition.canonical_admissible_fiber_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

For an arbitrary readout q and admissibility predicate Adm, the public statement exposes both dependent-sum equivalences and their forward and inverse computation rules.

The ordinary equivalence is the frozen family source of truth. The second equivalence sends an admissible state to its readout, its state, its admissibility evidence, and the reflexive fiber witness.

Each equivalence is unique among equivalences satisfying those computation rules. No surjectivity, section, quotient, or choice is assumed.

References

• Truth anchor: D5/S3/ConceptDynamics/Fibers/CanonicalAdmissibleFiberDecomposition.AdmissibleConceptFiber
• Truth anchor: D5/S3/ConceptDynamics/Fibers/CanonicalAdmissibleFiberDecomposition.canonical_admissible_fiber_decomposition
• Dependency: D5/S3/ConceptDynamics/Fibers/CanonicalDependentFiberEquivalence