eulerQ3_eq_2
plain-language theorem explainer
eulerQ3_eq_2 establishes that the Euler characteristic of the Q₃ configuration equals 2. Researchers deriving topology from the Recognition Science forcing chain would cite this equality when confirming that χ(Q₃) matches the value for S². The proof reduces to a single decide tactic on the integer arithmetic of the upstream definition.
Claim. $χ(Q_3) = 2$, where $χ(Q_3) = V - E + F$ evaluates to $8 - 12 + 6$.
background
The TopologyFromRS module identifies five canonical topological invariants (Euler characteristic, fundamental group, homology, cohomology, homotopy type) with configuration dimension D = 5. Upstream, eulerQ3 is defined as the integer expression 8 - 12 + 6, whose doc-comment states it computes the Euler characteristic V - E + F for Q₃. The module documentation notes that this value equals 2 and matches χ(S²).
proof idea
This is a one-line wrapper that applies the decide tactic to verify the equality between the predefined eulerQ3 integer and 2.
why it matters
The result supplies the euler_Q3 field inside the topologyCert definition, which certifies that all five invariants align with RS predictions. It directly supports the module claim that χ(Q₃) = 2 equals the Euler characteristic of S², advancing the derivation of topology from the RS functional equation and the eight-tick octave. It touches the open question of extracting the remaining four invariants from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.