four_plus_one
The arithmetic identity 4 + 1 = 5 confirms extension from four classical virtues to a total of five under the config dimension. Researchers mapping Aristotelian ethics to Recognition Science would cite it to anchor the virtue count. A single decision tactic verifies the equality without external lemmas.
claimIn the natural numbers the classical four virtues plus one integrating virtue sum to five: $4 + 1 = 5$.
background
The module treats five canonical virtues as an extension of the classical Aristotelian quartet, aligned with configDim D = 5. The virtues are prudence (phronesis), justice (dikaiosunē), fortitude (andreia), temperance (sōphrosynē), and practical wisdom (hexis) as the integrating fifth. Recognition Science frames practical wisdom as the element that completes the set to match the dimension pattern.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic statement.
why it matters in Recognition Science
The identity populates the CardinalVirtuesCert structure and the cardinalVirtuesCert definition, both of which require the sum to certify the five-virtue count. It supplies the D = 5 pattern that extends the classical four, consistent with the framework's dimension assignments. The result closes a local counting step but leaves open how the fifth virtue maps onto physical forcing-chain steps.
scope and limits
- Does not derive the virtues from any forcing-chain step.
- Does not assign physical units or mass formulas to the virtues.
- Does not prove that the listed five virtues are the only possible set.
Lean usage
def exampleCert : CardinalVirtuesCert where five_virtues := cardinalVirtue_count four_plus_one := four_plus_oneformal statement (Lean)
30theorem four_plus_one : (4 : ℕ) + 1 = 5 := by decide
proof body
31