The library documents itself · Numeric & optimization
stzMathClaim
20 own methods · 0 forms written with extensions, listed under their method
the source: base/math/stzMathClaim.ring(opens in a new tab) · All classes · The area reference: Numeric & optimization
Under each method, its extensions (Q CS XT Z ZZ IB W U): bold and ticked, it exists; struck, it does not. The extensions and what they mean
Examples: 0 come from the library's tests; 15 were composed from each method's signature and run for this page, on a fresh object, for example o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2"). 5 methods have none yet. Examples run on 2026-10-03 12:54 inside the library at commit 0e72e2e2c.
Method
Explanation, as the source carries it
init
(no comment in the source: the name reads as a sentence) initno extension
Kind
(no comment in the source: the name reads as a sentence) kindno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Kind()
#--> identitycomposed from the signature, run for this pageRelation
(no comment in the source: the name reads as a sentence) relationno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Relation()
#--> =composed from the signature, run for this pageLhs
(no comment in the source: the name reads as a sentence) lhsno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Lhs()
#--> 3^2 + 4^2 + 1composed from the signature, run for this pageRhs
(no comment in the source: the name reads as a sentence) rhsno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Rhs()
#--> 5^2composed from the signature, run for this pageOver
(no comment in the source: the name reads as a sentence) overno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Over()
#--> realcomposed from the signature, run for this pageVars
(no comment in the source: the name reads as a sentence) varsno extension
Label
(no comment in the source: the name reads as a sentence) labelno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Label()
#--> 3^2 + 4^2 + 1 = 5^2composed from the signature, run for this pageTactic
(no comment in the source: the name reads as a sentence) tacticno extension
Statement
(no comment in the source: the name reads as a sentence) statementno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Statement()
#--> 3^2 + 4^2 + 1 = 5^2composed from the signature, run for this pageSamplePoints
the points the floor samples: one for a closed statement, sixteen per variable otherwise, integers where the domain is integersno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? @@( o1.SamplePoints() )
#--> [ [ 0 ] ]composed from the signature, run for this pageCheck
the floor's verdict: every sampled point, the first counterexample keptno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? @@( o1.Check() )
#--> [ [ "verdict", 0 ], [ "route", "numeric floor" ], [ "points", 1 ], [ "evidence", "the sides are 26 and 25" ], [ "counterexample", [ 0 ] ] ]composed from the signature, run for this pageIsTrue
(no comment in the source: the name reads as a sentence) is trueno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.IsTrue()
#--> 0composed from the signature, run for this pageLastCheck
(no comment in the source: the name reads as a sentence) last checkno extension
TheoremName
THE DOOR: the Lean statement, and the verdict when Lean is presentno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.TheoremName()
#--> claim_3_2_4_2_1_5_2composed from the signature, run for this pageLeanTactic
the tactic: the author's, or the one the kind and the variables call forno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.LeanTactic()
#--> norm_numcomposed from the signature, run for this pageLeanStatement
(no comment in the source: the name reads as a sentence) lean statementno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.LeanStatement()
#--> ((3^2 + 4^2 + 1 : ℝ) = 5^2)composed from the signature, run for this pageToLean
(no comment in the source: the name reads as a sentence) to leanno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.ToLean()
#--> theorem claim_3_2_4_2_1_5_2 : ((3^2 + 4^2 + 1 : ℝ) = 5^2) := by norm_numcomposed from the signature, run for this pageCheckWithLean
through the door: a proof when Lean is here, the door's name when it is not; the floor's verdict rides along either wayno extension
Why
(no comment in the source: the name reads as a sentence) whyno extension
composed example
o1 = new stzMathClaim("3^2 + 4^2 + 1 = 5^2")
? o1.Why()
#--> an identity over the reals, '3^2 + 4^2 + 1 = 5^2': FALSE on the floor, the sides are 26 and 25; the Lean door is open (lean at C:\Lean\elan\bin/lean.exe, project at C:\Lean\stz_lean)composed from the signature, run for this page