eulerQ3
plain-language theorem explainer
The declaration defines the Euler characteristic of the three-cube Q₃ as the integer 2. A researcher working on Recognition Science topology cites this value when confirming that Q₃ reproduces the Euler characteristic of the 2-sphere. The definition is a direct arithmetic evaluation of the standard formula applied to the cube's vertex, edge, and face counts.
Claim. The Euler characteristic of the three-cube is defined by $Q_3$ Euler characteristic $V - E + F = 8 - 12 + 6 = 2$.
background
The module Topology from RS states that five canonical topological invariants correspond to configuration dimension D = 5. The Euler characteristic is one such invariant. For the 3-cube Q₃ the value follows the combinatorial formula V - E + F with V = 8, E = 12, F = 6. The module records that this equals 2 and matches the Euler characteristic of the 2-sphere S².
proof idea
The definition is a direct integer arithmetic expression evaluating 8 - 12 + 6.
why it matters
This definition supplies the concrete value required by the downstream TopologyCert structure, which asserts five invariants together with the Euler characteristic of Q₃ equal to 2. It supports the reproduction of S² topology for three spatial dimensions in the forcing chain at step T8. The sibling theorem eulerQ3_eq_2 then proves the equality by decision procedure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.