Encyclopedia Foundation Foundation Singular Prism Prism Comp Face Top

ARTICLE 3 claims 3 theorems

Foundation Singular Prism Prism Comp Face Top

A small identity about the edges of a geometric prism turns out to be the hinge that makes the whole framework's counting machinery consistent.

Verify this page

The top face rule

A prism is a shape made by sliding one copy of a flat polygon along a straight line. In topology, the standard object is the product of a triangle with a unit interval, and its boundary consists of a top face, a bottom face, and side faces. The declaration prism_comp_face_top states a precise rule about how the top face interacts with the map that slides the prism back down to its base. It says that composing the prism map that starts at the first vertex with the face map that ends at the first vertex gives exactly the identity map on the base paired with the constant map to 1, the top of the interval.

In plainer terms, if you take the prism built over a triangle, look at the edge that lies above the first vertex, and then project that edge straight down to the base triangle, you land exactly on the original base point. The formula is (prism (0 : Fin (n + 1))).comp (face (0 : Fin (n + 2))) = (ContinuousMap.id _).prodMk (ContinuousMap.const _ 1). The left side is the composition of two maps: first the face map that sends the base triangle into the prism as its bottom edge, then the prism map that sends that edge up to the top. The right side says the result is just the identity on the base triangle together with the constant value 1, meaning the point ends up at the top of the interval and stays at its original base coordinate.

This identity is one of several similar statements in the framework's library that govern how the prism decomposition maps behave. Its companion, prism_comp_face_bot, states the analogous rule for the bottom face, where the result lands at the constant 0 instead of 1. Together with prism_comp_face_of_le and prism_comp_face_of_gt, which handle the side faces, these rules give a complete description of how the prism maps interact with all boundary faces. The top-face rule is the one that pins down the behavior at the upper end of the interval, and it is what makes the chain homotopy construction in the library close properly.

In Recognition Science, this declaration is part of the framework's foundation for singular prism theory. The framework models continuous shapes as discrete combinatorial objects, and the prism maps are the bridge between a shape and its one-dimensional thickening. The top-face rule is a machine-checked theorem in the framework's library of formal theorems, meaning it has been verified by a computer to follow from the definitions without gaps. It is not an assumption or a conjecture; it is a proved consequence of the way the prism and face maps are defined.

What the declaration does not claim is broader significance beyond this specific algebraic identity. It does not say anything about the physical world, about recognition cost, about the golden ratio, or about the number of spatial dimensions. It is a technical lemma about the composition of two continuous maps on standard simplices. Its role is to make the machinery of the framework's singular chain complex work correctly, not to carry any empirical or physical content by itself.

THEOREM prism_comp_face_top · IndisputableMonolith/Foundation/SingularPrism.lean
prism_comp_face_top · IndisputableMonolith/Foundation/SingularPrism.lean:163 
/-- Top of the prism: `prism 0 ∘ face 0 = (x ↦ (x, 1))`. -/
theorem prism_comp_face_top :
    (prism (0 : Fin (n + 1))).comp (face (0 : Fin (n + 2))) =
      (ContinuousMap.id _).prodMk (ContinuousMap.const _ 1) := by
  refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
  · show stdSimplex.map (Fin.predAbove 0) (stdSimplex.map (Fin.succAbove 0) x) = x
    refine map_map_eq_self _ _ (fun k => ?_) x
    apply Fin.ext
    simp only [coe_predAbove, coe_succAbove, Fin.val_zero]
    split_ifs <;> omega
  · show prismSndFun 0 (stdSimplex.map (Fin.succAbove 0) x) = 1
    rw [prismSndFun_map_succAbove]
    calc ∑ m with (0 : Fin (n + 1)).castSucc < (0 : Fin (n + 2)).succAbove m, x m
        = ∑ m, x m := by
          apply Finset.sum_congr _ fun _ _ => rfl
          rw [Finset.filter_true_of_mem]
          intro m _
          simp only [Fin.lt_def, coe_succAbove, Fin.val_castSucc, Fin.val_zero]
          split_ifs <;> omega
      _ = 1 := x.2.2
THEOREM prism_comp_face_bot · IndisputableMonolith/Foundation/SingularPrism.lean
prism_comp_face_bot · IndisputableMonolith/Foundation/SingularPrism.lean:184 
/-- Bottom of the prism: `prism (last) ∘ face (last) = (x ↦ (x, 0))`. -/
theorem prism_comp_face_bot :
    (prism (Fin.last n)).comp (face (Fin.last (n + 1))) =
      (ContinuousMap.id _).prodMk (ContinuousMap.const _ 0) := by
  refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
  · show stdSimplex.map (Fin.predAbove (Fin.last n))
        (stdSimplex.map (Fin.succAbove (Fin.last (n + 1))) x) = x
    refine map_map_eq_self _ _ (fun k => ?_) x
    apply Fin.ext
    have hk := k.isLt
    simp only [coe_predAbove, coe_succAbove, Fin.val_last]
    split_ifs <;> omega
  · show prismSndFun (Fin.last n) (stdSimplex.map (Fin.succAbove (Fin.last (n + 1))) x) = 0
    rw [prismSndFun_map_succAbove]
    apply Finset.sum_eq_zero
    intro m hm
    exfalso
    rw [Finset.mem_filter] at hm
    have hm' := hm.2
    have hm2 := m.isLt
    rw [Fin.lt_def] at hm'
    revert hm'
    simp only [coe_succAbove, Fin.val_castSucc, Fin.val_last]
    split_ifs
    all_goals omega
THEOREM prism_comp_face_of_le · prism_comp_face_of_gt · IndisputableMonolith/Foundation/SingularPrism.lean
prism_comp_face_of_le · IndisputableMonolith/Foundation/SingularPrism.lean:233 
/-- Commutation with lower faces (`j ≤ i`): the composite of a prism map
with a low face factors through the prism one dimension down.  This matches
the `(i, j)` terms of `∂P` with `j < i+1` against the terms of `P∂`. -/
theorem prism_comp_face_of_le {i : Fin (n + 1)} {j : Fin (n + 2)}
    (hij : j ≤ i.castSucc) :
    (prism i.succ).comp (face j.castSucc) =
      ((face j).prodMap (ContinuousMap.id I)).comp (prism i) := by
  have hij' : (j : ℕ) ≤ (i : ℕ) := by simpa [Fin.le_def] using hij
  refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
  · show stdSimplex.map (Fin.predAbove i.succ)
        (stdSimplex.map (Fin.succAbove j.castSucc) x) =
      stdSimplex.map (Fin.succAbove j) (stdSimplex.map (Fin.predAbove i) x)
    refine map_map_eq_map_map _ _ _ _ (fun k => ?_) x
    apply Fin.ext
    have hk := k.isLt
    simp only [coe_predAbove, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
    split_ifs <;> omega
  · show prismSndFun i.succ (stdSimplex.map (Fin.succAbove j.castSucc) x) =
      prismSndFun i x
    rw [prismSndFun_map_succAbove, prismSndFun]
    refine Finset.sum_congr (Finset.filter_congr fun m _ => ?_) fun _ _ => rfl
    have hm := m.isLt
    simp only [Fin.lt_def, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
    split_ifs <;> omega
prism_comp_face_of_gt · IndisputableMonolith/Foundation/SingularPrism.lean:258 
/-- Commutation with high faces (`j > i`): the composite of a prism map
with a high face factors through the prism one dimension down.  This
matches the `(i, j)` terms of `∂P` with `j > i+1` against the terms of
`P∂`. -/
theorem prism_comp_face_of_gt {i : Fin (n + 1)} {j : Fin (n + 2)}
    (hij : i.castSucc < j) :
    (prism i.castSucc).comp (face j.succ) =
      ((face j).prodMap (ContinuousMap.id I)).comp (prism i) := by
  have hij' : (i : ℕ) < (j : ℕ) := by simpa [Fin.lt_def] using hij
  refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
  · show stdSimplex.map (Fin.predAbove i.castSucc)
        (stdSimplex.map (Fin.succAbove j.succ) x) =
      stdSimplex.map (Fin.succAbove j) (stdSimplex.map (Fin.predAbove i) x)
    refine map_map_eq_map_map _ _ _ _ (fun k => ?_) x
    apply Fin.ext
    have hk := k.isLt
    simp only [coe_predAbove, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
    split_ifs <;> omega
  · show prismSndFun i.castSucc (stdSimplex.map (Fin.succAbove j.succ) x) =
      prismSndFun i x
    rw [prismSndFun_map_succAbove, prismSndFun]
    refine Finset.sum_congr (Finset.filter_congr fun m _ => ?_) fun _ _ => rfl
    have hm := m.isLt
    simp only [Fin.lt_def, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
    split_ifs <;> omega

What this page does not claim

This declaration does not assert any physical fact about the world. It does not imply anything about recognition cost, the golden ratio, or spatial dimensions. It is not an assumption but a proved consequence of the definitions of the prism and face maps.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SingularPrism.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND