Foundation Singular Prism Prism Comp Face Bot

The bottom face of a prism

In topology, a prism is a way to interpolate between two continuous maps: take the product of a space with the unit interval, and slide from one map at the bottom to another at the top. The declaration prism_comp_face_bot is a theorem in the framework's machine-checked library of formal theorems. It states that composing the prism construction with the bottom face map equals the identity map on the space paired with the constant function at 0. In plain terms: if you start at the bottom of the prism, you get exactly the starting map, with the interval coordinate pinned to 0.

This is a boundary condition, one of the two essential checks that a prism is doing its job. The companion theorem prism_comp_face_top handles the top face, pinning the interval coordinate to 1. Together they ensure the prism connects its two ends correctly. The framework proves these identities for the standard simplex, the building block of singular homology, which is the classical tool for turning a topological space into a sequence of abelian groups that record its holes.

The theorem is a formal statement about continuous maps between standard simplices. It does not claim anything about the physical world, about recognition, or about the cost function that drives the framework's other results. It is a piece of foundational mathematics, checked by the machine, that the framework uses as a stepping stone for deeper constructions like chain homotopies. The declaration itself is a small, precise fact: the bottom face of a prism is the identity at level zero.

/-- 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

/-- 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

What this page does not claim

The theorem says nothing about recognition, cost, or any physical constant. The theorem does not establish that the prism construction is unique or that it satisfies any property beyond the stated boundary condition. The theorem does not prove that the bottom face map is an isomorphism or that the prism is invertible.

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: